\begin{tabbing}
$\forall$${\it es}$:ES, $P$:(E$\rightarrow\mathbb{P}$), $R$:(E$\rightarrow$E$\rightarrow\mathbb{P}$).
\\[0ex]($\forall$$e$:E. Dec($P$($e$)))
\\[0ex]$\Rightarrow$ ($\forall$$e$, ${\it e'}$:E. Dec($R$(${\it e'}$,$e$)))
\\[0ex]$\Rightarrow$ $R$ =$>$ $\lambda$$x$,$y$. ($x$ $<$ $y$)
\\[0ex]$\Rightarrow$ Trans(E;$x$,$y$.$R$($x$,$y$))
\\[0ex]$\Rightarrow$ \=($\forall$$a$, $b$, $e$:E.\+
\\[0ex]($\forall$$x$, $y$:E. $x$ c$\leq$ $e$ $\Rightarrow$ $y$ c$\leq$ $e$ $\Rightarrow$ $P$($x$) $\Rightarrow$ $P$($y$) $\Rightarrow$ ((($x$ $R$ $y$) $\vee$ ($x$ = $y$)) $\vee$ ($y$ $R$ $x$)))
\\[0ex]$\Rightarrow$ ($R$($e$,$a$) \& $R$($e$,$b$))
\\[0ex]$\Rightarrow$ ($P$($e$) \& $P$($a$) \& $P$($b$))
\\[0ex]$\Rightarrow$ ($\forall$$z$:E. $\neg$($R$($e$,$z$) \& $R$($z$,$a$) \& $P$($z$)))
\\[0ex]$\Rightarrow$ ($\forall$$z$:E. $\neg$($R$($e$,$z$) \& $R$($z$,$b$) \& $P$($z$)))
\\[0ex]$\Rightarrow$ ($a$ = $b$))
\-\\[0ex]$\Rightarrow$ \=($\forall$$m$, ${\it m'}$:E.\+
\\[0ex]$P$($m$) $\Rightarrow$ $P$(${\it m'}$) $\Rightarrow$ ($\forall$$e$:E. ($e$ $R$ $m$) $\Rightarrow$ ($\neg$$P$($e$))) $\Rightarrow$ ($\forall$$e$:E. ($e$ $R$ ${\it m'}$) $\Rightarrow$ ($\neg$$P$($e$))) $\Rightarrow$ ($m$ = ${\it m'}$))
\-\\[0ex]$\Rightarrow$ ($\forall$$e$, ${\it e'}$:E. $P$($e$) $\Rightarrow$ $P$(${\it e'}$) $\Rightarrow$ ((($e$ $R$ ${\it e'}$) $\vee$ ($e$ = ${\it e'}$)) $\vee$ (${\it e'}$ $R$ $e$)))
\end{tabbing}